Search for: All records

Abstract Real-world work environments require operators to perform multiple tasks with continual support from an automated system. Eye movement is often used as a surrogate measure of operator attention, yet conventional summary measures such as percent dwell time do not capture dynamic transitions of attention in complex visual workspace. This study analyzed eye movement data collected in a controlled a MATB-II task environment using gaze transition entropy analysis. In the study, human subjects performed a compensatory tracking task, a system monitoring task, and a communication task concurrently. The results indicate that both gaze transition entropy and stationary gaze entropy, measures of randomness in eye movements, decrease when the compensatory tracking task required more continuous monitoring. The findings imply that gaze transition entropy reflects attention allocation of operators performing dynamic operational tasks consistently. 

The implementation of automation will enable Advanced Air Mobility (AAM), which could alter the human's responsibilities from those of an active controller to a passive monitor of vehicles. Mature AAM operations will likely rely on both experienced and novice operators to supervise multiple aircraft. As AAM constitutes a complex and increasingly autonomous system, the human operator's set of responsibilities will transition from those of a controller, to a manager, and eventually to an assistant to highly automated systems. The development of AAM will require system designers to characterize these three sets of human responsibilities. The present work proposes different human responsibilities across various roles (i.e., pilot in command, system operator, system assistant) in the context of AAM along with pertinent attention-related constructs that could contribute to each of the three identified roles of AAM operators including situation awareness, workload, complacency, and vigilance. 

Adversarial computations are a widely studied class of computations where resource-bounded probabilistic adversaries have access to oracles, i.e., probabilistic procedures with private state. These computations arise routinely in several domains, including security, privacy and machine learning. In this paper, we develop program logics for reasoning about adversarial computations in a higher-order setting. Our logics are built on top of a simply typed λ-calculus extended with a graded monad for probabilities and state. The grading is used to model and restrict the memory footprint and the cost (in terms of oracle calls) of computations. Under this view, an adversary is a higher-order expression that expects as arguments the code of its oracles. We develop unary program logics for reasoning about error probabilities and expected values, and a relational logic for reasoning about coupling-based properties. All logics feature rules for adversarial computations, and yield guarantees that are valid for all adversaries that satisfy a fixed resource policy. We prove the soundness of the logics in the category of quasi-Borel spaces, using a general notion of graded predicate liftings, and we use logical relations over graded predicate liftings to establish the soundness of proof rules for adversaries. We illustrate the working of our logics with simple but illustrative examples.